;;;===========================================================================
;;;
;;; SES 1 Theorem
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 14/05/10 || End date: 19/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "cone-equivalence-theorem-structure")


(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring-R *) => *)
 ;; Addition operation ring
 ((addition-ring-R * *)=> *)
 ;; Product operation ring
 ((product-ring-R * *) => *)
 ;; Inverse ring
 ((inverse-R *) => *)
 ;; Zero element ring
 ((zero-element-R ) => *)
 ;; Unit element ring
 ((unit-R )=> *)

 ;;--------------------------------------------------
 ;; We want to find the homotopye equivalence CA <<= DA =>> HA
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; CA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-CA * *) => *)
 ;; Group Operation 
 ((group-operation-CA * * *) => *)
 ;; Zero element
 ((zero-CA *) => *)
 ;; External multiplication
 ((external-CA * * *) => *)
 ;; Inverse element
 ((inverse-CA * *) => *)

 ;;--------------------------------------------------
 ;; The CA differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-CA * *) => *)



 ;;--------------------------------------------------
 ;; Second homotopy equivalence CB <<= DB =>> HB
 ;;--------------------------------------------------


 ;;--------------------------------------------------
 ;; CB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-CB * *) => *)
 ;; Group Operation 
 ((group-operation-CB * * *) => *)
 ;; Zero element
 ((zero-CB *) => *)
 ;; External multiplication
 ((external-CB * * *) => *)
 ;; Inverse element
 ((inverse-CB * *) => *)

 ;;--------------------------------------------------
 ;; The CB differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-CB * *) => *)

 ;;--------------------------------------------------
 ;; DB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-DB * *) => *)
 ;; Group Operation 
 ((group-operation-DB * * *) => *)
 ;; Zero element
 ((zero-DB *) => *)
 ;; External multiplication
 ((external-DB * * *) => *)
 ;; Inverse element
 ((inverse-DB * *) => *)

 ;;--------------------------------------------------
 ;; The DB differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-DB * *) => *)

  ;;--------------------------------------------------
 ;; HB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-HB * *) => *)
 ;; Group Operation 
 ((group-operation-HB * * *) => *)
 ;; Zero element
 ((zero-HB *) => *)
 ;; External multiplication
 ((external-HB * * *) => *)
 ;; Inverse element
 ((inverse-HB * *) => *)

 ;;--------------------------------------------------
 ;; The HB differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-HB * *) => *)

 
 ;;--------------------------------------------------
 ;; Third homotopy equivalence CC <<= DC =>> HC
 ;;--------------------------------------------------


 ;;--------------------------------------------------
 ;; C_C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C_C * *) => *)
 ;; Group Operation 
 ((group-operation-C_C * * *) => *)
 ;; Zero element
 ((zero-C_C *) => *)
 ;; External multiplication
 ((external-C_C * * *) => *)
 ;; Inverse element
 ((inverse-C_C * *) => *)

 ;;--------------------------------------------------
 ;; The C_C differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C_C * *) => *)

 ;;--------------------------------------------------
 ;; DC Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-DC * *) => *)
 ;; Group Operation 
 ((group-operation-DC * * *) => *)
 ;; Zero element
 ((zero-DC *) => *)
 ;; External multiplication
 ((external-DC * * *) => *)
 ;; Inverse element
 ((inverse-DC * *) => *)

 ;;--------------------------------------------------
 ;; The DC differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-DC * *) => *)

  ;;--------------------------------------------------
 ;; HC Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-HC * *) => *)
 ;; Group Operation 
 ((group-operation-HC * * *) => *)
 ;; Zero element
 ((zero-HC *) => *)
 ;; External multiplication
 ((external-HC * * *) => *)
 ;; Inverse element
 ((inverse-HC * *) => *)

 ;;--------------------------------------------------
 ;; The HC differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-HC * *) => *)

 
 ;;--------------------------------------------------
 ;; Morphisms of the first homotopy equivalence
 ;;--------------------------------------------------


 ;;--------------------------------------------------
 ;; The lfB morphism
 ;;--------------------------------------------------

 ;; The function
 ((lfB * *) => *)

 ;;--------------------------------------------------
 ;; The lgB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((lgB * *) => *)


 ;;--------------------------------------------------
 ;; The lhB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((lhB * *) => *)

 ;;--------------------------------------------------
 ;; The rfB morphism
 ;;--------------------------------------------------

 ;; The function
 ((rfB * *) => *)

 ;;--------------------------------------------------
 ;; The rgB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((rgB * *) => *)


 ;;--------------------------------------------------
 ;; The rhB CB morphism
 ;;--------------------------------------------------

 ;; The function
 ((rhB * *) => *)



 ;;--------------------------------------------------
 ;; The lfC morphism
 ;;--------------------------------------------------

 ;; The function
 ((lfC * *) => *)

 ;;--------------------------------------------------
 ;; The lgC C_C morphism
 ;;--------------------------------------------------

 ;; The function
 ((lgC * *) => *)


 ;;--------------------------------------------------
 ;; The lhC C_C morphism
 ;;--------------------------------------------------

 ;; The function
 ((lhC * *) => *)

 ;;--------------------------------------------------
 ;; The rfC morphism
 ;;--------------------------------------------------

 ;; The function
 ((rfC * *) => *)

 ;;--------------------------------------------------
 ;; The rgC C_C morphism
 ;;--------------------------------------------------

 ;; The function
 ((rgC * *) => *)


 ;;--------------------------------------------------
 ;; The rhC C_C morphism
 ;;--------------------------------------------------

 ;; The function
 ((rhC * *) => *)

 ;;--------------------------------------------------
 ;; sigma : A -> B
 ;;--------------------------------------------------

 ((sigma * *) => *)

 ;;--------------------------------------------------
 ;; j : B -> A
 ;;--------------------------------------------------

 ((j * *) => *)
 
 ;;--------------------------------------------------
 ;; rho : B -> C
 ;;--------------------------------------------------

 ((rho * *) => *)

 ;;--------------------------------------------------
 ;; i : C -> B
 ;;--------------------------------------------------

 ((i * *) => *)
 

 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring-R (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring-R (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring-R (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse-R (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element-R nil
	  0))

 ;; Unit element ring
 (local (defun unit-R nil
	  1))

 ;;--------------------------------------------------
 ;; CA Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-CA (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-CA (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-CA (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-CA (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-CA (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The CA differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-CA (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; CB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-CB (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-CB (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-CB (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-CB (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-CB (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The CB differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-CB (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; DB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-DB (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-DB (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-DB (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-DB (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-DB (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The DB differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-DB (n a)
	  (declare (ignore n a))
	  0))


  ;;--------------------------------------------------
 ;; HB Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-HB (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-HB (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-HB (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-HB (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-HB (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The HB differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-HB (n a)
	  (declare (ignore n a))
	  0))
 


 ;;--------------------------------------------------
 ;; C_C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C_C (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C_C (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C_C (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C_C (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C_C (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C_C differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C_C (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; DC Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-DC (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-DC (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-DC (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-DC (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-DC (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The DC differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-DC (n a)
	  (declare (ignore n a))
	  0))


  ;;--------------------------------------------------
 ;; HC Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-HC (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-HC (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-HC (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-HC (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-HC (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The HC differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-HC (n a)
	  (declare (ignore n a))
	  0))
 

 ;;--------------------------------------------------
 ;; The lfB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lfB (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lgB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lgB (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lhB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lhB (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rfB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rfB (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rgB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rgB (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The rhB morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rhB (n a)
	  (declare (ignore n a))
	  0))




 ;;--------------------------------------------------
 ;; The lfC morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lfC (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lgC morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lgC (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lhC morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lhC (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rfC morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rfC (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rgC morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rgC (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lhC morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rhC (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; sigma : A -> B
 ;;--------------------------------------------------

 (local (defun sigma (n a)
	(declare (ignore n a))
	  0
	))

 ;;--------------------------------------------------
 ;; j : B -> A
 ;;--------------------------------------------------

 (local (defun j (n a)
	(declare (ignore n a))
	  0
	))
 
 
 ;;--------------------------------------------------
 ;; rho : B -> C
 ;;--------------------------------------------------

(local (defun rho (n a)
	(declare (ignore n a))
	  0
	))
 

 ;;--------------------------------------------------
 ;; i : C -> B
 ;;--------------------------------------------------

(local (defun i (n a)
	(declare (ignore n a))
	  0
	))
 

 

  ;;************************************************** 
  ;; Properties
  ;;************************************************** 

(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring-R :addition-ring 'addition-ring-R :zero-element 'zero-element-R
		    :inverse 'inverse-R :product-ring 'product-ring-R :unit 'unit-R
		    :inv-cc 'inv-cA :group-operation-cc 'group-operation-ca :zero-cc 'zero-ca :external-cc 'external-ca
		    :inverse-cc 'inverse-ca :d-cc 'd-ca)
 'CA)

(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DB 'group-operation-DB 'zero-DB 'external-DB 'inverse-DB 'd-DB )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-CB 'group-operation-CB 'zero-CB 'external-CB 'inverse-CB 'd-CB )
  'lfB  'lgB  'lhB
  )
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DB 'group-operation-DB 'zero-DB 'external-DB 'inverse-DB 'd-DB )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-HB 'group-operation-HB 'zero-HB 'external-HB 'inverse-HB 'd-HB )
  'rfB  'rgB  'rhB
  ))
 'homotopy-equivalence-B
   )


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DC 'group-operation-DC 'zero-DC 'external-DC 'inverse-DC 'd-DC )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-C_C 'group-operation-C_C 'zero-C_C 'external-C_C 'inverse-C_C 'd-C_C )
  'lfC  'lgC  'lhC
  )
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-DC 'group-operation-DC 'zero-DC 'external-DC 'inverse-DC 'd-DC )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
    'inv-HC 'group-operation-HC 'zero-HC 'external-HC 'inverse-HC 'd-HC )
  'rfC  'rgC  'rhC
  ))
 'homotopy-equivalence-C
   )



(check-chain-complex-morphism-degree-0-p
(chain-complex-morphism-degree-0 
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-CB 'group-operation-CB 'zero-CB 'external-CB 'inverse-CB 'd-CB )
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-CA 'group-operation-CA 'zero-CA 'external-CA 'inverse-CA 'd-CA )
 'j) 'j)


(check-chain-complex-morphism-degree-0-p
(chain-complex-morphism-degree-0 
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-C_C 'group-operation-C_C 'zero-C_C 'external-C_C 'inverse-C_C 'd-C_C )
 (chain-complex 'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 'inv-CB 'group-operation-CB 'zero-CB 'external-CB 'inverse-CB 'd-CB )
 'i) 'i)


(check-morphism-degree-0-p
(morphism-degree-0 'inv-CA 'inv-CB 'sigma  'group-operation-CA 'group-operation-CB
		   'external-CA 'external-CB 'inv-ring-R
		   'zero-CA 'zero-CB 'inverse-CA 'inverse-CB )
'sigma
)

(check-morphism-degree-0-p
(morphism-degree-0  'inv-CB 'inv-C_C 'rho  'group-operation-CB 'group-operation-C_C
		    'external-CB 'external-C_C 'inv-ring-R
		    'zero-CB 'zero-C_C 'inverse-CB 'inverse-C_C )
'rho
)

(defthm rho-i
  (implies (and (inv-C_C n a)
		(integerp n))
	   (equal (rho n (i n a))
		  a)))

(defthm i-rho+sigma-j
  (implies (and (inv-CB n a)
		(integerp n))
	   (equal (group-operation-CB n (i n (rho n a))
				      (sigma n (j n a)))
		  a)))

(defthm j-sigma
  (implies (and (inv-CA n a)
		(integerp n))
	   (equal (j n (sigma n a))
		  a)))


(defthm rho-sigma
  (implies (and (inv-CA n a)
		(integerp n))
	   (equal (rho n (sigma n a))
		  (zero-C_C n))))


(defthm j-i
  (implies (and (inv-C_C n c)
		(integerp n))
	   (equal (j n (i n c))
		  (zero-CA n))))

)

;;;**************************************************
;;;
;;; Definition of the Equivalence of the Cone(i)
;;;
;;;**************************************************



(defthm prop1 (IMPLIES (AND (INV-C_C N A)
              (INV-C_C N B)
              (INV-C_C N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C_C N (GROUP-OPERATION-C_C N A B) C)
                (GROUP-OPERATION-C_C N A (GROUP-OPERATION-C_C N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))


(defthm prop2-aux
  (IMPLIES (AND (INV-C_C N A) (INTEGERP N))
         (INV-C_C (+ N -1) (D-C_C N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))


(defthm prop2
  (IMPLIES (AND (INV-C_C N A) (INTEGERP N))
         (INV-C_C (+ -1 n) (D-C_C N A)))
 :hints (("Goal" :use ((:instance prop2-aux)))))


(defthm prop3 (IMPLIES (AND (INV-CB N A)
              (INV-CB N B)
              (INV-CB N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CB N (GROUP-OPERATION-CB N A B) C)
                (GROUP-OPERATION-CB N A (GROUP-OPERATION-CB N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))

(defthm prop4 (IMPLIES (AND (INV-DB N A)
              (INV-DB N B)
              (INV-DB N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DB N (GROUP-OPERATION-DB N A B) C)
                (GROUP-OPERATION-DB N A (GROUP-OPERATION-DB N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))

(defthm prop5 (IMPLIES (AND (INV-HB N A)
              (INV-HB N B)
              (INV-HB N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-HB N (GROUP-OPERATION-HB N A B) C)
                (GROUP-OPERATION-HB N A (GROUP-OPERATION-HB N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop6 (IMPLIES (AND (INV-DC N A)
              (INV-DC N B)
              (INV-DC N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DC N (GROUP-OPERATION-DC N A B) C)
                (GROUP-OPERATION-DC N A (GROUP-OPERATION-DC N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))

(defthm prop7 (IMPLIES (AND (INV-HC N A)
              (INV-HC N B)
              (INV-HC N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-HC N (GROUP-OPERATION-HC N A B) C)
                (GROUP-OPERATION-HC N A (GROUP-OPERATION-HC N B C)))) 
:hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))

(defthm prop8-aux
  (IMPLIES (AND (INV-CB N A) (INTEGERP N))
         (INV-CB (+ N -1) (D-CB N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop8
  (IMPLIES (AND (INV-CB N A) (INTEGERP N))
         (INV-CB (+ -1 n) (D-CB N A)))
 :hints (("Goal" :use ((:instance prop8-aux)))))

(defthm prop9-aux
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ N -1) (D-DB N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop9
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ -1 n) (D-DB N A)))
 :hints (("Goal" :use ((:instance prop9-aux)))))


(defthm prop10-aux
  (IMPLIES (AND (INV-HB N A) (INTEGERP N))
         (INV-HB (+ N -1) (D-HB N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop10
  (IMPLIES (AND (INV-HB N A) (INTEGERP N))
         (INV-HB (+ -1 n) (D-HB N A)))
 :hints (("Goal" :use ((:instance prop10-aux)))))


(defthm prop11-aux
  (IMPLIES (AND (INV-DC N A) (INTEGERP N))
         (INV-DC (+ N -1) (D-DC N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))


(defthm prop11
  (IMPLIES (AND (INV-DC N A) (INTEGERP N))
         (INV-DC (+ -1 n) (D-DC N A)))
 :hints (("Goal" :use ((:instance prop11-aux)))))


(defthm prop12-aux
  (IMPLIES (AND (INV-HC N A) (INTEGERP N))
         (INV-HC (+ N -1) (D-HC N A)))
 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))


(defthm prop12
  (IMPLIES (AND (INV-HC N A) (INTEGERP N))
         (INV-HC (+ -1 n) (D-HC N A)))
 :hints (("Goal" :use ((:instance prop12-aux)))))

(defthm prop13-aux
  (IMPLIES (AND (INV-DC N A) (INTEGERP N))
	   (INV-DC (+ N 1) (LHC N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))


(defthm prop13
  (IMPLIES (AND (INV-DC N A) (INTEGERP N))
	   (INV-DC (+ 1 N) (LHC N A)))
  :hints (("Goal" :use ((:instance prop13-aux)))))


(defthm prop14-aux
  (IMPLIES (AND (INV-DC N A) (INTEGERP N))
         (INV-DC (+ N 1) (RHC N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))


(defthm prop14
  (IMPLIES (AND (INV-DC N A) (INTEGERP N))
         (INV-DC (+ 1 N) (RHC N A)))
  :hints (("Goal" :use ((:instance prop14-aux)))))



(defthm prop15-aux
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ n 1) (LHB N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop15
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ 1 n) (LHB N A)))
  :hints (("Goal" :use ((:instance prop15-aux)))))


(defthm prop16-aux
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ n 1) (RHB N A)))
  :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-B-is-an-homotopy-equivalence|)))))


(defthm prop16
  (IMPLIES (AND (INV-DB N A) (INTEGERP N))
         (INV-DB (+ 1 n) (rHB N A)))
  :hints (("Goal" :use ((:instance prop16-aux)))))


(definstance-*CONE-REDUCTION-THEOREM*
  ((inv-ring-Z inv-ring-R)
    (addition-ring-Z addition-ring-R)
    (product-ring-Z product-ring-R)
    (inverse-Z inverse-R)
    (zero-element-Z zero-element-R)
    (unit-Z unit-R)
    (inv-C1 inv-CB)
    (group-operation-C1 group-operation-CB)
    (zero-C1 zero-CB)
    (external-C1 external-CB)
    (inverse-C1 inverse-CB)
    (d-C1 d-CB)
    (inv-D1 inv-DB)
    (group-operation-D1 group-operation-DB)
    (zero-D1 zero-DB)
    (external-D1 external-DB)
    (inverse-D1 inverse-DB)
    (d-D1 d-DB)
    (inv-H1 inv-HB)
    (group-operation-H1 group-operation-HB)
    (zero-H1 zero-HB)
    (external-H1 external-HB)
    (inverse-H1 inverse-HB)
    (d-H1 d-HB)
    (inv-C2 inv-C_C)
    (group-operation-C2 group-operation-C_C)
    (zero-C2 zero-C_C)
    (external-C2 external-C_C)
    (inverse-C2 inverse-C_C)
    (d-C2 d-C_C)
    (inv-D2 inv-DC)
    (group-operation-D2 group-operation-DC)
    (zero-D2 zero-DC)
    (external-D2 external-DC)
    (inverse-D2 inverse-DC)
    (d-D2 d-DC)
    (inv-H2 inv-HC)
    (group-operation-H2 group-operation-HC)
    (zero-H2 zero-HC)
    (external-H2 external-HC)
    (inverse-H2 inverse-HC)
    (d-H2 d-HC)
    (lf1 lfb)
    (lg1 lgb)
    (lh1 lhb)
    (rf1 rfb)
    (rg1 rgb)
    (rh1 rhb)
    (lf2 lfc)
    (lg2 lgc)
    (lh2 lhc)
    (rf2 rfc)
    (rg2 rgc)
    (rh2 rhc)
    (phi-c2-c1 i))
  "-cone-SES1")




;;;**************************************************
;;;
;;; Definition of the functions of Reduction Cone(i) =>> CA
;;;
;;;**************************************************



(defun f-cone-A (n a)
  (j n (car a))
  )



(defun g-cone-A (n a)
  (list (sigma n a)
	(inverse-C_C (+ n -1) (rho (+ n -1) (d-CB n (sigma n a)))))
  )

(defun h-cone-cone (n a)
  (list (zero-CB (+ n 1))
	(rho n (car a)))
  )



;;;**************************************************
;;;
;;; Auxiliar lemmas
;;;
;;;**************************************************


(defthm group-operation-cb-commutativity
  (IMPLIES (AND (INV-CB N A)
		(INV-CB N B)
		(integerp n))
         (EQUAL (GROUP-OPERATION-CB N A B)
                (GROUP-OPERATION-CB N B A))))

(in-theory (disable group-operation-cb-commutativity))

(defthm lemma1
  (IMPLIES (AND (INV-CB N (car A))
		(INV-CB N (car B) )
		(INV-CB N (car C))
		(integerp n))
         (EQUAL (GROUP-OPERATION-CB N (car c) (GROUP-OPERATION-CB N (car A) (car b)))
                (GROUP-OPERATION-CB N (car a) (GROUP-OPERATION-CB N (car b) (car c))))) 
:hints (("Goal" :use ((:instance prop3)
		      (:instance  group-operation-cb-commutativity
				  (a (car c))
				  (b (GROUP-OPERATION-CB N (car A) (car b))))))))

(defthm lemma1-bis
  (IMPLIES (AND (INV-CB N a)
		(INV-CB N b )
		(INV-CB N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-CB N c (GROUP-OPERATION-CB N a b))
                (GROUP-OPERATION-CB N a (GROUP-OPERATION-CB N b c)))) 
:hints (("Goal" :use ((:instance prop3)
		      (:instance  group-operation-cb-commutativity
				  (a c)
				  (b (GROUP-OPERATION-CB N a b)))))))


(defthm group-operation-cc-commutativity
  (IMPLIES (AND (INV-C_c N A)
		(INV-C_C N B)
		(integerp n))
         (EQUAL (GROUP-OPERATION-C_c N A B)
                (GROUP-OPERATION-C_c N B A))))

(in-theory (disable group-operation-cc-commutativity))

(defthm lemma2
  (IMPLIES (AND (INV-C_C (+ -1 N) (cadr A))
		(INV-C_C (+ -1 N) (cadr B) )
		(INV-C_C (+ -1 N) (cadr C))
		(integerp n))
         (EQUAL (GROUP-OPERATION-C_C (+ -1 N) (cadr c) (GROUP-OPERATION-C_C (+ -1 N) (cadr A) (cadr b)))
                (GROUP-OPERATION-C_C (+ -1 N) (cadr a) (GROUP-OPERATION-C_C (+ -1 N) (cadr b) (cadr c))))) 
:hints (("Goal" :use ((:instance  group-operation-cc-commutativity
				  (n (+ -1 N))
				  (a (cadr c))
				  (b (GROUP-OPERATION-C_C (+ -1 N) (cadr A) (cadr b))))))))



(defthm group-operation-ca-commutativity
  (IMPLIES (AND (INV-Ca N A)
		(INV-Ca N B)
		(integerp n))
         (EQUAL (GROUP-OPERATION-Ca N A B)
                (GROUP-OPERATION-Ca N B A))))

(in-theory (disable group-operation-ca-commutativity))


(defthm prop17 (IMPLIES (AND (INV-Ca N A)
              (INV-Ca N B)
              (INV-Ca N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CA N (GROUP-OPERATION-CA N A B) C)
                (GROUP-OPERATION-CA N A (GROUP-OPERATION-CA N B C)))) 
:hints (("Goal" :use ((:instance |CA-is-a-chain-complex|)))))

(defthm lemma3
  (IMPLIES (AND (INV-Ca N a)
		(INV-Ca N b)
		(INV-Ca N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-Ca N c (GROUP-OPERATION-Ca N a b))
                (GROUP-OPERATION-Ca N a (GROUP-OPERATION-Ca N b c)))) 
:hints (("Goal" :use (
		      (:instance  group-operation-ca-commutativity
				  (a c)
				  (b (GROUP-OPERATION-Ca N a b)))))))



(defthm lemma4
  (implies (and (inv-ca n a)
		(integerp n))
	   (inv-ca (+ n -1) (d-ca n a)))
:hints (("Goal" :use ((:instance |CA-is-a-chain-complex|)))))

(defthm lemma4-aux
  (implies (and (inv-ca n a)
		(integerp n))
	   (inv-ca (+ -1 n) (d-ca n a)))
:hints (("Goal" :use ((:instance lemma4)))))


(defthm lemma5
  (implies (and (inv-cb n a)
		(integerp n))
	   (inv-c_c n (rho n a))))

(defthm lemma-aux-5-help
  (implies (integerp n)
	   (equal (+ -1 1 N) n))
  :rule-classes nil)

(defthm lemma5-aux
  (implies (and (inv-cb n a)
		(integerp n))
	   (inv-c_c (+ -1 1 N) (rho n a)))
  :hints (("Goal" :use ((:instance lemma-aux-5-help)
			(:instance lemma5)
			))))



(defthm lemma6
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-C_C N (RHO N a)
				       (RHO N b))
		  (GROUP-OPERATION-C_C (+ -1 1 N)
				       (RHO N a)
				       (RHO N b))
		  ))
  :hints (("Goal" :use ((:instance lemma-aux-5-help)))))


(defthm lemma7
  (implies (and (inv-ring-r r)
		(integerp n))
	   (equal (external-cb n r (zero-cb n))
		  (zero-cb n))))


(defthm lemma8
  (implies (integerp n)
  (EQUAL (EXTERNAL-C_C N R (RHO N (CAR A)))
       (EXTERNAL-C_C (+ -1 1 N)
                     R (RHO N (CAR A)))))
  :hints (("Goal" :use ((:instance lemma-aux-5-help)))))

(defthm lemma9
  (implies (integerp n)
	   (EQUAL (ZERO-C_C (+ -1 1 N))
		  (ZERO-C_C N)))
    :hints (("Goal" :use ((:instance lemma-aux-5-help)))))
	   

(defthm lemma10
  (implies (integerp n)
  (EQUAL  (INVERSE-C_C (+ -1 1 N)
                    (RHO N (CAR A)))
	  (INVERSE-C_C N (RHO N (CAR A)))))
  :hints (("Goal" :use ((:instance lemma-aux-5-help)))))


(defthm lemma-11-help
  (implies (integerp n)
	   (equal (+ 1 N) (+ -1 1 1 N)))
  :rule-classes nil)

(defthm lemma11
  (implies (integerp n)
	   (EQUAL (ZERO-C_C (+ -1 1 1 N))
		  (ZERO-C_C (+ 1 N))))
    :hints (("Goal" :use ((:instance lemma-11-help)))))
	   



(defthm lemma12
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(inv-cb n c)
		(integerp n))
	   (equal (group-operation-cb n a (group-operation-cb n b c))
		  (group-operation-cb n b (group-operation-cb n a c))))
  :hints (("Goal" :use 
	   ((:instance group-operation-cb-commutativity (b c) (a b))
	    (:instance lemma1-bis (b c) (c b))	    
	    ))))

(defthm lemma12-bis
(IMPLIES
 (AND (EQUAL (LIST (CAR A) (CADR A)) A)
      (INV-CB N (CAR A))
      (INV-C_C (+ -1 N) (CADR A))
      (EQUAL (LIST (CAR B) (CADR B)) B)
      (INV-CB N (CAR B))
      (INV-C_C (+ -1 N) (CADR B))
      (INTEGERP N))
 (EQUAL
     (GROUP-OPERATION-CB
          (+ -1 N)
          (D-CB N (CAR A))
          (GROUP-OPERATION-CB (+ -1 N)
                              (D-CB N (CAR B))
                              (GROUP-OPERATION-CB (+ -1 N)
                                                  (I (+ -1 N) (CADR A))
                                                  (I (+ -1 N) (CADR B)))))
     (GROUP-OPERATION-CB
          (+ -1 N)
          (D-CB N (CAR A))
          (GROUP-OPERATION-CB (+ -1 N)
                              (I (+ -1 N) (CADR A))
                              (GROUP-OPERATION-CB (+ -1 N)
                                                  (D-CB N (CAR B))
                                                  (I (+ -1 N) (CADR B)))))))

)

(in-theory (disable lemma12))

(defthm lemma13
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-ca n (zero-ca n) a)
		  a
		  )))
		


(defthm lemma14-help
  (implies (integerp n)
	   (equal (+ -1 1 -1 N)
		  (+ -1 N)))
  :rule-classes nil)

(defthm lemma14
  (implies (and (inv-c_c (+ -1 N) a)
		(inv-c_c (+ -1 N) b)
		(integerp n))
	   (equal (inverse-C_C (+ -1 N) (group-operation-C_C (+ -1 1 -1 N) a b))
		  (group-operation-C_C (+ -1 N) (inverse-C_C (+ -1 N) a)  (inverse-C_C (+ -1 N) b))))
  :hints (("Goal" :use ((:instance lemma14-help)))))
  
(defthm lemma15-help1
  (implies (and (inv-Cb n a)
		(integerp n))
	   (equal (d-ca n (j n a))
		  (j (+ -1 n) (d-cb n a))))
  :hints (("Goal" :use (:instance |J-is-a-chain-complex-morphism-of-degree-0|))))


(defthm lemma15
  (implies (and (inv-CA n a)
		(integerp n))
	   (equal (sigma (+ -1 n) (d-ca n a))
		  (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
  :hints (("Goal" :in-theory (disable lemma15-help1)
	   :use ((:instance j-sigma)
		 (:instance lemma15-help1 (a (sigma n a)))))))
	  

(defthm lemma16
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-cb (+ -1 n)
				      (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))				      
				      (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))				      
				      )
		  (d-cb n (sigma n a))
		  ))
  :hints (("Goal" :use ((:instance i-rho+sigma-j (a (d-cb n (sigma n a)))
				   (n (+ -1 n)))))))



(defthm lemma17
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(integerp n))
	   (equal (group-operation-cb n 
				      (group-operation-cb n a b)
				      (inverse-cb n a))
		  b))
  :hints (("Goal" :use ((:instance group-operation-cb-commutativity (a a) (b b))
			(:instance prop3 (a b) (b a) (c (inverse-cb n a))))))
	   )



(defthm lemma18
  (implies (and (inv-ca n a)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-CB (+ -1 N)
				(D-CB N (SIGMA N A))
				(INVERSE-CB (+ -1 N)
					    (I (+ -1 N)
					       (RHO (+ -1 N) (D-CB N (SIGMA N A))))))
	    (SIGMA (+ -1 N)
		   (J (+ -1 N) (D-CB N (SIGMA N A))))))
  :hints (("Goal" :use ((:instance lemma15)
			(:instance lemma16)
			(:instance lemma17
				   (n (+ -1 n))
				   (a (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a)))))
				   (b (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a)))))))))
  )



(defthm lemma19-help1
  (implies (integerp n)
	   (equal (+ 1 -1 N) n))
  :rule-classes nil)

(defthm lemma19-help2
  (implies (integerp n)
	   (EQUAL (ZERO-C_C (+ 1 -1 N))
		  (ZERO-C_C N)))
    :hints (("Goal" :use ((:instance lemma19-help1)))))


(defthm lemma19-help3
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (GROUP-OPERATION-CB N (ZERO-CB (+ 1 -1 N))
                      (GROUP-OPERATION-CB (+ -1 1 N)
                                          (ZERO-CB (+ -1 1 N))
                                          (I (+ -1 1 N) (RHO N a))))
		  (GROUP-OPERATION-CB N (ZERO-CB n)
                      (GROUP-OPERATION-CB n
                                          (ZERO-CB n)
                                          (I n (RHO N a))))))
  :hints (("Goal" :use ((:instance lemma9)
			(:instance lemma19-help1)
			(:instance lemma19-help2)
			(:instance LEMMA-AUX-5-HELP)))))


(defthm lemma19-help4
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (group-operation-cb n (zero-cb n) a)
		  a)))

(defthm lemma19
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (GROUP-OPERATION-CB N (ZERO-CB (+ 1 -1 N))
                      (GROUP-OPERATION-CB (+ -1 1 N)
                                          (ZERO-CB (+ -1 1 N))
                                          (I (+ -1 1 N) (RHO N a))))
		  (I n (RHO N a))))
  :hints (("Goal" :use ((:instance lemma19-help3)
			(:instance lemma19-help4 (a (I n (RHO N a))))
			))))


(defthm lemma20
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(inv-cb n c)
		(integerp n)
		(equal (group-operation-cb n a b) c))
	   (equal (group-operation-cb n c (inverse-cb n b))
		  a)))


(defthm lemma21
  (implies (and (inv-cb n a)
		(integerp n))
	   (EQUAL
  (GROUP-OPERATION-CB N (ZERO-CB (+ 1 -1 N))
                      (GROUP-OPERATION-CB (+ -1 1 N)
                                          (ZERO-CB (+ -1 1 N))
                                          (I (+ -1 1 N) (RHO N a))))
  (GROUP-OPERATION-CB N a
                      (INVERSE-CB N (SIGMA N (J N a))))))
  :hints (("Goal" :use ((:instance lemma19)
			(:instance i-rho+sigma-j)
			(:instance lemma20
				   (a (I N (RHO N A)))
				   (b (SIGMA N (J N A)))
				   (c a))))))


(defthm lemma22-help
  (IMPLIES
   (AND (INV-C_c N A)
	(INV-C_c N B)
	(INV-C_c N C)
	(INTEGERP N))
   (EQUAL (GROUP-OPERATION-C_c N (GROUP-OPERATION-C_c N A B)
			      C)
	  (GROUP-OPERATION-C_c N A (GROUP-OPERATION-C_c N B C))))
  :HINTS
               (("Goal"
                 :USE
                 ((:INSTANCE
                     |HOMOTOPY-EQUIVALENCE-C-is-an-homotopy-equivalence|)))))

(defthm lemma-22-help-2
  (implies (integerp n)
	   (equal (+ -1 -1 1 N) (+ -1 N)))
  :rule-classes nil)

(defthm lemma22
  (implies (and (inv-cb n (car gnrt))
		(inv-c_c (+ -1 n) (cadr gnrt))
		(integerp n))
	   (equal (GROUP-OPERATION-C_C
		   (+ -1 N)
		   (GROUP-OPERATION-C_C (+ -1 N)
					(CADR GNRT)
					(RHO (+ -1 N) (D-CB N (CAR GNRT))))
		   (INVERSE-C_C (+ -1 -1 1 N)
				(D-C_C (+ -1 1 N) (RHO N (CAR GNRT)))))
		  (group-operation-c_c (+ -1 N)
				       (CADR GNRT)
				       (GROUP-OPERATION-C_C (+ -1 N)
							    (RHO (+ -1 N) (D-CB N (CAR GNRT)))
							    (INVERSE-C_C (+ -1 N) 
								      (D-C_C (+ -1 1 N) (RHO N (CAR GNRT)))))
				       )))
  :hints (("Goal" :use ((:instance lemma-22-help-2)
			(:instance lemma22-help (n (+ -1 N))
				   (a (CADR GNRT))
				   (b (RHO (+ -1 N) (D-CB N (CAR GNRT))))
				   (c (INVERSE-C_C (+ -1 N) 
								      (D-C_C (+ -1 1 N) (RHO N (CAR GNRT)))))))))
  )


(defthm lemma23-help1
  (implies (and (inv-c_C n a)
		(integerp n))
	   (equal (inverse-c_c n (inverse-c_c n a))
		  a)))

(defthm lemma23
  (implies (and (inv-cb n (car gnrt))
		(integerp n))
	   (equal(INVERSE-C_C (+ -1 N)
			      (INVERSE-C_C (+ -1 N)
					   (RHO (+ -1 N)
						(D-CB N (SIGMA N (J N (CAR GNRT)))))))
		 (RHO (+ -1 N)
		      (D-CB N (SIGMA N (J N (CAR GNRT)))))))
  :hints (("Goal" :use ((:instance lemma23-help1 (n (+ -1 N))
				   (a (RHO (+ -1 N)
					   (D-CB N (SIGMA N (J N (CAR GNRT))))))))))
)


(defthm lemma-24-help-1
  (implies (integerp n)
	   (equal (+ -1 1 -1 N) (+ -1 N)))
  :rule-classes nil)

(defthm lemma24-help-2
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(integerp n))
	   (equal (group-operation-c_c (+ -1 n)
				      (rho (+ -1 n) (d-cb n a))				      
				      (rho (+ -1 n) (d-cb n b))				      
				      )
		  (rho (+ -1 n) (d-cb n (group-operation-cb n a b)))))
  :hints (("Goal" :in-theory (disable lemma6)
	   :use (:instance lemma-24-help-1))))
 
	  

(defthm lemma24
  (implies (and (inv-cb n a)
		(integerp n))
	   (equal (group-operation-c_C (+ -1 n)
				      (rho (+ -1 n) (d-cb n (i n (rho n a))))				      
				      (rho (+ -1 n) (d-cb n (sigma n (j n a))))				      
				      )
		  (rho (+ -1 n) (d-cb n a))))
  :hints (("Goal" :in-theory (disable rho-i LEMMA5 lemma6)
	   :use ((:instance i-rho+sigma-j)
		 (:instance lemma24-help-2 (a (i n (rho n a)))
			    (b (sigma n (j n a))))))))




(defthm lemma25
  (implies (and (inv-Cb n a)
		(integerp n))
	   (equal (D-C_C (+ -1 1 N) (RHO N a))
		  (rho (+ -1 n) (d-cb n (i n (rho n a))))))
  :hints (("Goal" :use ((:instance lemma-aux-5-help)
			(:instance rho-i (a (D-C_C n (RHO N a)))))))
)



(defthm lemma26
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n))
	   (equal (group-operation-c_c n 
				      (group-operation-c_c n a b)
				      (inverse-c_c n a))
		  b))
  :hints (("Goal" :use ((:instance group-operation-cc-commutativity (a a) (b b))
			(:instance lemma22-help (a b) (b a) (c (inverse-c_c n a))))))
	   )



(defthm lemma27
  (implies (and (inv-cb n a)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-C_C (+ -1 N)
                        (RHO (+ -1 N) (D-CB N a))
                        (INVERSE-C_C (+ -1 N)
                                     (D-C_C (+ -1 1 N) (RHO N a))))
	    (RHO (+ -1 N)
		 (D-CB N (SIGMA N (J N a))))))
  :hints (("Goal" :use ((:instance lemma24)
			(:instance lemma25)
			(:instance lemma26
				   (n (+ -1 n))
				   (a (rho (+ -1 n) (d-cb n (i n (rho n a)))))
				   (b (RHO (+ -1 N)
					   (D-CB N (SIGMA N (J N a)))))))))
  )
 


(defthm lemma28
  (implies (and (inv-c_c n a)
		(inv-c_c n b)
		(integerp n)
		(equal (group-operation-c_c n a b) (zero-c_c n)))
	   (equal (inverse-c_c n b) a))
  :rule-classes nil)



(defthm lemma29-help1
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ -1 -1 N)
		   (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
		   (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		   )
		  (group-operation-c_c
		   (+ -1 -1 N)
		    (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		    (rho (+ -1 -1 N) (d-cb (+ -1 n) (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))))
		   ))))

(in-theory (disable lemma24-help-2 lemma29-help1))


(defthm lemma29-help2
  (implies (and (inv-cb n a)
		(inv-cb n b)
		(integerp n))
	   (equal (group-operation-c_c (+ -1 n) 
				       (rho (+ -1 n) (d-cb n a))
				       (rho (+ -1 n) (d-cb n b)))
		  (rho (+ -1 n) (d-cb n (group-operation-cb n a b))))))



(defthm lemma29-help3
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ -1 -1 N)
		    (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		    (rho (+ -1 -1 N) (d-cb (+ -1 n) (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))))
		   )
		  (rho (+ -1 -1 N) (d-cb (+ -1 n)
					 (group-operation-cb
					  (+ -1 n) 
					  (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))
					  (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a)))))
		   ))))
  :hints (("Goal" :in-theory (disable lemma29-help1)
	   :use ((:instance lemma29-help2
			    (n (+ -1 n))
			    (a (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a)))))
			    (b (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))))) ))
)

(in-theory (enable lemma29-help1))


(defthm lemma29-help4
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ -1 -1 N)
		   (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
		   (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		   )
		  (rho (+ -1 -1 N) (d-cb (+ -1 n)
					 (group-operation-cb
					  (+ -1 n) 
					  (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))
					  (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a)))))
		   ))))
  :hints (("Goal" :in-theory (disable rho-i prop8 prop2)
	   :use ((:instance lemma29-help2)
		 (:instance lemma29-help3)))))
			

(defthm lemma29-help5
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ -1 -1 N)
		   (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
		   (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		   )
		  (rho (+ -1 -1 N) (d-cb (+ -1 n)
					 (group-operation-cb
					  (+ -1 n) 
					  (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
					  (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))
					  )
		   ))))
  :hints (("Goal" :in-theory (disable lemma16)
	   :use ((:instance lemma29-help4)
		 (:instance group-operation-cb-commutativity 
			    (n (+ -1 n))
			    (a (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a)))))
			    (b (i (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))))))))


(defthm lemma29-help6
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ -1 -1 N)
		   (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
		   (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		   )
		  (rho (+ -1 -1 N) (d-cb (+ -1 n)
					 (d-cb n (sigma n a))
		   ))))
  :hints (("Goal" :in-theory (disable lemma16)
	   :use ((:instance lemma29-help5)
		 (:instance i-rho+sigma-j 
			    (n (+ -1 n))
			    (a (d-cb n (sigma n a))))))))



(defthm lemma29
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (group-operation-c_c
		   (+ -1 -1 N)
		   (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
		   (rho (+ -1 -1 N) (d-cb (+ -1 n) (sigma (+ -1 n) (j (+ -1 n) (d-cb n (sigma n a))))))
		   )
		  (zero-c_c (+ -1 -1 N))))
  :hints (("Goal" 
	   :use ((:instance lemma29-help6)
		 ))))



(defthm lemma30
  (implies (and (inv-ca n a)
		(integerp n))
	   (equal (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a))))
		  (INVERSE-C_C (+ -1 -1 N)
                    (RHO (+ -1 -1 N)
                         (D-CB (+ -1 N)
                               (SIGMA (+ -1 N)
                                      (J (+ -1 N) (D-CB N (SIGMA N A))))))))
	   )
  :hints (("Goal" :use ((:instance lemma29)
			(:instance lemma28
				   (n (+ -1 -1 N))
				   (a (d-c_c (+ -1 n) (rho (+ -1 n) (d-cb n (sigma n a)))))
				   (b (RHO (+ -1 -1 N)
                         (D-CB (+ -1 N)
                               (SIGMA (+ -1 N)
                                      (J (+ -1 N) (D-CB N (SIGMA N A)))))))))))

)




;;;**************************************************
;;;
;;; Definition of the Reduction Cone(i) =>> CA
;;;
;;;**************************************************

(in-theory (disable 
		    lemma29-help2))

(defreduction 
   inv-ring-R addition-ring-R zero-element-R inverse-R product-ring-R unit-R
   inv-CONE-CONE-C2-C1-CONE-SES1 group-operation-CONE-CONE-C2-C1-CONE-SES1
   zero-CONE-CONE-C2-C1-CONE-SES1 external-CONE-CONE-C2-C1-CONE-SES1
   inverse-CONE-CONE-C2-C1-CONE-SES1 d-CONE-CONE-C2-C1-CONE-SES1
   inv-CA group-operation-CA zero-CA external-CA inverse-CA d-CA 
   f-cone-A  g-cone-A h-cone-cone 
   cone->A
   :HINTS
   (("Subgoal 65.2" :USE ((:INSTANCE lemma1)))
    ("Subgoal 65.1" :USE ((:INSTANCE lemma2)))    
    ("Subgoal 4.2" :USE ((:instance lemma21 (a (CAR GNRT)))))
    ("Subgoal 4.1" :USE ((:instance lemma22)
			 (:instance lemma27 (a (CAR GNRT)))))
    ))


;;;**************************************************
;;;
;;; Definition of the new Reduction 
;;; Cone(di) =>> CA  (Cone(di) =>> Cone(i) =>> CA) 
;;;
;;;**************************************************


;(include-book "SES1-Theorem-help")

(include-book "cmps-reductions-structure")


(defthm property1
  (IMPLIES (AND (INV-CB N a)
              (INV-CB N b)
              (INV-CB N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CB N a (GROUP-OPERATION-CB N b c))
		(GROUP-OPERATION-CB N c (GROUP-OPERATION-CB N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-cb-commutativity
				   (a c)
				   (b (GROUP-OPERATION-CB N a b)))))))



(defthm property2
  (IMPLIES (AND (INV-C_c N a)
              (INV-C_c N b)
              (INV-C_c N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C_C N a (GROUP-OPERATION-C_c N b c))
		(GROUP-OPERATION-C_C N c (GROUP-OPERATION-C_c N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-cc-commutativity
				   (a c)
				   (b (GROUP-OPERATION-C_c N a b)))))))


(defthm property3
  (IMPLIES (AND 
	    (INV-ca N a)
              (INV-ca N b)
              (INV-ca N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-CA N a (GROUP-OPERATION-ca N b c))
		(GROUP-OPERATION-CA N c (GROUP-OPERATION-ca N a b))))
  
  :hints (("Goal" :in-theory (disable |CONE->A-is-a-reduction|)
	   :use ((:instance group-operation-ca-commutativity
				   (a c)
				   (b (GROUP-OPERATION-ca N a b)))))))


(DEFTHM
  LEMMA19-bis
  (IMPLIES
   (AND (INV-CB N A) (INTEGERP N))
   (EQUAL (GROUP-OPERATION-CB n
			       (ZERO-CB (+ 1 -1 N))
			       (I (+ -1 1 N) (RHO N A)))
	  (I N (RHO N A))))
  :HINTS
  (("Goal"
    :USE ((:INSTANCE LEMMA-AUX-5-HELP)
	  (:instance lemma19-help1)
	  ))))

(defthm property4
  (implies (and (inv-cb n a)
		(integerp n))
	   (EQUAL
	    (GROUP-OPERATION-CB n
				(ZERO-CB (+ 1 -1 N))
				(I (+ -1 1 N) (RHO N a)))
	    
	    (GROUP-OPERATION-CB N a
				(INVERSE-CB N (SIGMA N (J N a))))))
  :hints (("Goal" :use ((:instance lemma19-bis)
			(:instance i-rho+sigma-j)
			(:instance lemma20
				   (a (I N (RHO N A)))
				   (b (SIGMA N (J N A)))
				   (c a))))))



(DEFTHM
  LEMMA22-bis
  (IMPLIES
   (AND (INV-CB N (CAR GNRT))
	(INV-C_C (+ -1 N) (CADR GNRT))
	(INTEGERP N))
   (EQUAL
    (GROUP-OPERATION-C_C
     (+ -1 N)
     (GROUP-OPERATION-C_C (+ -1 N)
			  (CADR GNRT)
			  (RHO (+ -1 N) (D-CB N (CAR GNRT))))
     (INVERSE-C_C (+ -1 -1 1 N)
		  (D-C_C n (RHO N (CAR GNRT)))))
    (GROUP-OPERATION-C_C
     (+ -1 N)
     (CADR GNRT)
     (GROUP-OPERATION-C_C
      (+ -1 N)
      (RHO (+ -1 N) (D-CB N (CAR GNRT)))
      (INVERSE-C_C (+ -1 N)
		   (D-C_C n
			  (RHO N (CAR GNRT))))))))
  :HINTS
  (("Goal"
                 :USE ((:INSTANCE LEMMA-22-HELP-2)
                       (:INSTANCE
			LEMMA22-HELP (N (+ -1 N))
			(A (CADR GNRT))
			(B (RHO (+ -1 N) (D-CB N (CAR GNRT))))
			(C (INVERSE-C_C (+ -1 N)
					(D-C_C n
					       (RHO N (CAR GNRT))))))))))


(DEFTHM
  LEMMA27-bis
  (IMPLIES
   (AND (INV-CB N A) (INTEGERP N))
   (EQUAL (GROUP-OPERATION-C_C
	   (+ -1 N)
	   (RHO (+ -1 N) (D-CB N A))
	   (INVERSE-C_C (+ -1 N)
			(D-C_C n (RHO N A))))
	  (RHO (+ -1 N)
	       (D-CB N (SIGMA N (J N A))))))
               :HINTS
               (("Goal"
                 :USE ((:INSTANCE LEMMA27)
                       (:instance lemma-aux-5-help)
                       ))))


(DEFTHM GROUP-OPERATION-dB-COMMUTATIVITY
  (IMPLIES (AND (INV-dB N A)
		(INV-dB N B)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-dB N A B)
		  (GROUP-OPERATION-dB N B A))))
				       
(defthm property5
  (IMPLIES (AND (INV-dB N a)
              (INV-dB N b)
              (INV-dB N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DB N a (GROUP-OPERATION-DB N b c))
		(GROUP-OPERATION-DB N c (GROUP-OPERATION-DB N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-db-commutativity
				   (a c)
				   (b (GROUP-OPERATION-DB N a b)))
			(:instance prop4)))))

(in-theory (disable |CONE->A-is-a-reduction|))

(DEFTHM GROUP-OPERATION-dc-COMMUTATIVITY
  (IMPLIES (AND (INV-dc N A)
		(INV-dc N B)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-dc N A B)
		  (GROUP-OPERATION-dc N B A))))

				       
(defthm property6
  (IMPLIES (AND (INV-dc N a)
              (INV-dc N b)
              (INV-dc N c)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-DC N a (GROUP-OPERATION-DC N b c))
		(GROUP-OPERATION-DC N c (GROUP-OPERATION-DC N a b))))
  
  :hints (("Goal" :use ((:instance group-operation-dc-commutativity
				   (a c)
				   (b (GROUP-OPERATION-DC N a b)))
			(:instance prop6)))))


(defthm property7-bis (IMPLIES
      (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	   (INTEGERP N))
      (EQUAL (D-CONE-CONE-D2-D1-CONE-SES1
	      (1- N)
	      (D-CONE-CONE-D2-D1-CONE-SES1 N A))
	     (ZERO-CONE-CONE-D2-D1-CONE-SES1 (1- (1- N)))))
     :hints (("Goal" :in-theory (disable zero-cone-cone-d2-d1-cone-ses1
					 D-CONE-CONE-D2-D1-CONE-SES1
					 INV-CONE-CONE-D2-D1-CONE-SES1
					 D-CONE-CONE-D2-D1-CONE-SES1))))


(in-theory (disable zero-cone-cone-d2-d1-cone-ses1
		    D-CONE-CONE-D2-D1-CONE-SES1
		    D-CONE-CONE-D2-D1-CONE-SES1))


(defthm property7
  (IMPLIES
      (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	   (INTEGERP N))
      (EQUAL (D-CONE-CONE-D2-D1-CONE-SES1
	      (+ -1 N)
	      (D-CONE-CONE-D2-D1-CONE-SES1 N A))
	     (ZERO-CONE-CONE-D2-D1-CONE-SES1 (+ -1 -1 N)))))


(in-theory (disable GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
		    INVERSE-CONE-CONE-D2-D1-CONE-SES1))



(defthm property8-help1
  (IMPLIES
   (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	(INV-CONE-CONE-D2-D1-CONE-SES1 N B)
	(INV-CONE-CONE-D2-D1-CONE-SES1 N C)
	(INTEGERP N))
   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
			      C)
	  (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N B C))))
  :HINTS
               (("Goal"
                 :USE
                 ((:INSTANCE
		   |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES1|)))))



(defthm property8-help2
  (IMPLIES
   (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	(INV-CONE-CONE-D2-D1-CONE-SES1 N B)
	(INV-CONE-CONE-D2-D1-CONE-SES1 N C)
	(INTEGERP N))
   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
			      C)
	  (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N B C))))
  :HINTS
               (("Goal"
                 :USE
                 ((:INSTANCE
                     |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES1|)))))



(defthm property8-help3
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	      (INV-CONE-CONE-D2-D1-CONE-SES1 N b)
              (INTEGERP N))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N 
							     (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
							     (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N B))
		  a))
  :hints (("Goal" :use ((:instance property8-help1 (a a) (b b))
			(:instance property8-help2  (a b) (b a) (c (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N B))))))
	   )


(defthm property8-help4
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	      (INV-CONE-CONE-D2-D1-CONE-SES1 N b)
              (INTEGERP N))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N 
							     (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
							     (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N a))
		  b))
  :hints (("Goal" :use ((:instance property8-help1 (a b) (b a))
			(:instance property8-help3 (a b) (b a))
			)))
	   )

(defthm property8-help5
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N
							     a
							     (ZERO-CONE-CONE-D2-D1-CONE-SES1 N)
							     )
		  a))
  :hints (("Goal"
                 :USE
                 ((:INSTANCE
                     |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES1|)))))

(defthm property8-help6
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N
							     (ZERO-CONE-CONE-D2-D1-CONE-SES1 N)
							     a)
		  a))
  :hints (("Goal"
                 :USE
                 ((:INSTANCE property8-help1 
			     (a (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))
			     (b a)
                     )
		  (:instance property8-help5)))))


(defthm property8-help7
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N 
							     (ZERO-CONE-CONE-D2-D1-CONE-SES1 N)
							     (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N a))
		  (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N a))))


(defthm property8-help8
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	      (INV-CONE-CONE-D2-D1-CONE-SES1 N b)
              (INTEGERP N)
	      (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
                     (ZERO-CONE-CONE-D2-D1-CONE-SES1 N)))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N 
							     (ZERO-CONE-CONE-D2-D1-CONE-SES1 N)
							     (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N a))
		  (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N 
							     (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
							     (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N a))
		  )))

(defthm property8-help9
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
	      (INV-CONE-CONE-D2-D1-CONE-SES1 N b)
              (INTEGERP N)
	      (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B)
                     (ZERO-CONE-CONE-D2-D1-CONE-SES1 N)))
	   (EQUAL (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N a)
		  b))
  :hints (("Goal" :in-theory (disable INV-CONE-CONE-D2-D1-CONE-SES1)
	   :use ((:instance property8-help8)
		 (:instance property8-help7)
		 (:instance property8-help4)))))


(defthm property9
  (IMPLIES
 (AND (EQUAL (LIST (CAR A) (CADR A)) A)
      (INV-DB N (CAR A))
      (INV-DC (+ -1 N) (CADR A))
      (INV-RING-R R)
      (INTEGERP N))
 (INV-CONE-CONE-D2-D1-CONE-SES1 N
                                (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R A))))


(in-theory (enable INV-CONE-CONE-D2-D1-CONE-SES1
		   D-CONE-CONE-D2-D1-CONE-SES1))


(defthm property10
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1 (+ -1 N)
                                        (D-CONE-CONE-D2-D1-CONE-SES1 N A))))
  

(in-theory (disable INV-CONE-CONE-D2-D1-CONE-SES1
		    EXTERNAL-CONE-CONE-D2-D1-CONE-SES1
		    D-CONE-CONE-D2-D1-CONE-SES1))


(in-theory (enable INV-CONE-CONE-D2-D1-CONE-SES1
		   ))

(defthm property11 
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CB N (LFB N (CAR A))))
)

(defthm property12
 (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-C_C (+ -1 N)
                  (LFC (+ -1 N) (CADR A))))
)


(in-theory (enable D-CONE-CONE-D2-D1-CONE-SES1))


(defthm property13
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (EQUAL (GROUP-OPERATION-CB (+ -1 N)
                                    (D-CB N (LFB N (CAR A)))
                                    (I (+ -1 N) (LFC (+ -1 N) (CADR A))))
                (LFB (+ -1 N)
                     (CAR (D-CONE-CONE-D2-D1-CONE-SES1 N A))))))


(defthm property14
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (EQUAL (INVERSE-C_C (+ -1 -1 N)
                             (D-C_C (+ -1 N)
                                    (LFC (+ -1 N) (CADR A))))
                (LFC (+ -1 -1 N)
                     (CADR (D-CONE-CONE-D2-D1-CONE-SES1 N A))))))
  
(defthm property15-aux
  (implies (and (inv-dc n a)
		(integerp n))
	   (inv-dc (+ n 1) (inverse-dc (+ n 1) (LHC n a)))))
  

(defthm property15-aux2
  (implies (and (inv-dc (+ -1 N) a)
		(integerp n))
	   (inv-dc (+ -1 1 N) (inverse-dc n (LHC (+ -1 N) a))))
  :hints (("Goal" :use ((:instance property15-aux (n (+ -1 N)))
			(:instance lemma-aux-5-help)
			(:instance lemma19-help1)))))

(defthm property15
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1
              (+ 1 N)
              (LIST (LHB N (CAR A))
                    (INVERSE-DC N (LHC (+ -1 N) (CADR A)))))))


(defthm property16
  (IMPLIES (AND (EQUAL (LIST (CAR A) (CADR A)) A)
              (INV-CB N (CAR A))
              (INV-C_C (+ -1 N) (CADR A))
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1 N
                                        (LIST (LGB N (CAR A))
                                              (LGC (+ -1 N) (CADR A))))))


(in-theory (enable GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1))


(defthm property17
  (IMPLIES (AND (EQUAL (LIST (CAR A) (CADR A)) A)
              (INV-CB N (CAR A))
              (INV-C_C (+ -1 N) (CADR A))
              (EQUAL (LIST (CAR B) (CADR B)) B)
              (INV-CB N (CAR B))
              (INV-C_C (+ -1 N) (CADR B))
              (INTEGERP N))
         (EQUAL (LIST (GROUP-OPERATION-DB N (LGB N (CAR A))
                                          (LGB N (CAR B)))
                      (GROUP-OPERATION-DC (+ -1 N)
                                          (LGC (+ -1 N) (CADR A))
                                          (LGC (+ -1 N) (CADR B))))
                (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
                     N
                     (LIST (LGB N (CAR A))
                           (LGC (+ -1 N) (CADR A)))
                     (LIST (LGB N (CAR B))
                           (LGC (+ -1 N) (CADR B)))))))


(in-theory (enable EXTERNAL-CONE-CONE-D2-D1-CONE-SES1))

(defthm property18
  (IMPLIES
 (AND (EQUAL (LIST (CAR A) (CADR A)) A)
      (INV-CB N (CAR A))
      (INV-C_C (+ -1 N) (CADR A))
      (INV-RING-R R)
      (INTEGERP N))
 (EQUAL (LIST (EXTERNAL-DB N R (LGB N (CAR A)))
              (EXTERNAL-DC (+ -1 N)
                           R (LGC (+ -1 N) (CADR A))))
        (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R
                                            (LIST (LGB N (CAR A))
                                                  (LGC (+ -1 N) (CADR A)))))))


(in-theory (enable ZERO-CONE-CONE-D2-D1-CONE-SES1))

(defthm property19
  (IMPLIES (INTEGERP N)
         (EQUAL (LIST (ZERO-DB N) (ZERO-DC (+ -1 N)))
                (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))))


(in-theory (enable INVERSE-CONE-CONE-D2-D1-CONE-SES1))


(defthm property20
  (IMPLIES
  (AND (EQUAL (LIST (CAR A) (CADR A)) A)
       (INV-CB N (CAR A))
       (INV-C_C (+ -1 N) (CADR A))
       (INTEGERP N))
  (EQUAL (LIST (INVERSE-DB N (LGB N (CAR A)))
               (INVERSE-DC (+ -1 N)
                           (LGC (+ -1 N) (CADR A))))
         (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N
                                            (LIST (LGB N (CAR A))
                                                  (LGC (+ -1 N) (CADR A)))))))
  

(in-theory (enable D-CONE-CONE-D2-D1-CONE-SES1))

(defthm property21
  (IMPLIES
     (AND (EQUAL (LIST (CAR A) (CADR A)) A)
          (INV-CB N (CAR A))
          (INV-C_C (+ -1 N) (CADR A))
          (INTEGERP N))
     (EQUAL (D-CONE-CONE-D2-D1-CONE-SES1 N
                                         (LIST (LGB N (CAR A))
                                               (LGC (+ -1 N) (CADR A))))
            (LIST (GROUP-OPERATION-DB (+ -1 N)
                                      (LGB (+ -1 N) (D-CB N (CAR A)))
                                      (LGB (+ -1 N) (I (+ -1 N) (CADR A))))
                  (INVERSE-DC (+ -1 -1 N)
                              (LGC (+ -1 -1 N)
                                   (D-C_C (+ -1 N) (CADR A))))))))


(in-theory (enable GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
		   INVERSE-CONE-CONE-D2-D1-CONE-SES1
		   INV-CONE-CONE-D2-D1-CONE-SES1
		   D-CONE-CONE-D2-D1-CONE-SES1))



(in-theory (enable INV-CONE-CONE-D2-D1-CONE-SES1
		   INVERSE-CONE-CONE-D2-D1-CONE-SES1
		   LH-CONES-CONE-SES1
		   LG-CONES-CONE-SES1
		   LF-CONES-CONE-SES1
		   ZERO-CONE-CONE-D2-D1-CONE-SES1
		   EXTERNAL-CONE-CONE-D2-D1-CONE-SES1))

(defthm property22
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1 (+ 1 N)
                                        (LH-CONES-CONE-SES1 N A))))
  

(defthm property23
  (IMPLIES (AND (INV-CONE-CONE-c2-c1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1 n
                                        (Lg-CONES-CONE-SES1 N A))))


(defthm property24
  (IMPLIES (AND (INV-CONE-CONE-d2-d1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-c2-c1-CONE-SES1 n
                                        (Lf-CONES-CONE-SES1 N A))))

(defthm property25
  (IMPLIES
  (AND (EQUAL (LIST (CAR A) (CADR A)) A)
       (INV-CB N (CAR A))
       (INV-C_C (+ -1 N) (CADR A))
       (EQUAL (LIST (CAR B) (CADR B)) B)
       (INV-CB N (CAR B))
       (INV-C_C (+ -1 N) (CADR B))
       (INTEGERP N))
  (EQUAL
       (LG-CONES-CONE-SES1 N
                           (LIST (GROUP-OPERATION-CB N (CAR A) (CAR B))
                                 (GROUP-OPERATION-C_C (+ -1 N)
                                                      (CADR A)
                                                      (CADR B))))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N (LG-CONES-CONE-SES1 N A)
                                                  (LG-CONES-CONE-SES1 N B)))))


(defthm property26
  (IMPLIES
   (AND (EQUAL (LIST (CAR A) (CADR A)) A)
        (INV-CB N (CAR A))
        (INV-C_C (+ -1 N) (CADR A))
        (INV-RING-R R)
        (INTEGERP N))
   (EQUAL (LG-CONES-CONE-SES1 N
                              (LIST (EXTERNAL-CB N R (CAR A))
                                    (EXTERNAL-C_C (+ -1 N) R (CADR A))))
          (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R (LG-CONES-CONE-SES1 N A)))))



(defthm property27
  (IMPLIES (INTEGERP N)
         (EQUAL (LG-CONES-CONE-SES1 N
                                    (LIST (ZERO-CB N) (ZERO-C_C (+ -1 N))))
                (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))))


(defthm property28
  (IMPLIES
     (AND (EQUAL (LIST (CAR A) (CADR A)) A)
          (INV-CB N (CAR A))
          (INV-C_C (+ -1 N) (CADR A))
          (INTEGERP N))
     (EQUAL (LG-CONES-CONE-SES1 N
                                (LIST (INVERSE-CB N (CAR A))
                                      (INVERSE-C_C (+ -1 N) (CADR A))))
            (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N (LG-CONES-CONE-SES1 N A)))))

(in-theory (disable INV-CONE-CONE-D2-D1-CONE-SES1
		    ZERO-CONE-CONE-D2-D1-CONE-SES1
		    D-CONE-CONE-D2-D1-CONE-SES1
		    INVERSE-CONE-CONE-D2-D1-CONE-SES1
		    EXTERNAL-CONE-CONE-D2-D1-CONE-SES1
		    GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
		    LG-CONES-CONE-SES1
		    LF-CONES-CONE-SES1 
		    LH-CONES-CONE-SES1))



;;|CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|

(definstance-*cmps*
  ((inv-ring-cmps inv-ring-R)
    (addition-ring-cmps addition-ring-R)
    (product-ring-cmps product-ring-R)
    (inverse-cmps inverse-R)
    (zero-element-cmps zero-element-R)
    (unit-cmps unit-R)
    (inv-top inv-CONE-CONE-D2-D1-CONE-SES1)
    (group-operation-top group-operation-CONE-CONE-D2-D1-CONE-SES1)
    (zero-top zero-CONE-CONE-D2-D1-CONE-SES1)
    (external-top external-CONE-CONE-D2-D1-CONE-SES1)
    (inverse-top inverse-CONE-CONE-D2-D1-CONE-SES1)
    (d-top d-CONE-CONE-D2-D1-CONE-SES1)
    (inv-middle inv-CONE-CONE-C2-C1-CONE-SES1) 
    (group-operation-middle group-operation-CONE-CONE-C2-C1-CONE-SES1)
    (zero-middle zero-CONE-CONE-C2-C1-CONE-SES1)
    (external-middle external-CONE-CONE-C2-C1-CONE-SES1)
    (inverse-middle inverse-CONE-CONE-C2-C1-CONE-SES1)
    (d-middle d-CONE-CONE-C2-C1-CONE-SES1)
    (inv-bottom inv-ca) 
    (group-operation-bottom group-operation-ca)
    (zero-bottom zero-ca)
    (external-bottom external-ca)
    (inverse-bottom inverse-ca)
    (d-bottom d-ca)
    (f1 f-cone-a)
    (g1 g-cone-a)
    (h1 h-cone-cone)
    (f2 lf-cones-cone-ses1)
    (g2 lg-cones-cone-ses1)
    (h2 lh-cones-cone-ses1)
    )
  "-cone-di-ca")





;;;**************************************************
;;;
;;; Definition of the Equivalence: 
;;; CA <<= Cone(i) <<= Cone(di) =>> Cone(hi)
;;;
;;;**************************************************

(in-theory (enable INV-CONE-CONE-D2-D1-CONE-SES1
		    ZERO-CONE-CONE-D2-D1-CONE-SES1
		    D-CONE-CONE-D2-D1-CONE-SES1
		    INVERSE-CONE-CONE-D2-D1-CONE-SES1
		    EXTERNAL-CONE-CONE-D2-D1-CONE-SES1
		    GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
		    LG-CONES-CONE-SES1
		    LF-CONES-CONE-SES1 
		    LH-CONES-CONE-SES1
		    inv-CONE-CONE-D2-D1-CONE-SES1 group-operation-CONE-CONE-D2-D1-CONE-SES1 zero-CONE-CONE-D2-D1-CONE-SES1 external-CONE-CONE-D2-D1-CONE-SES1 inverse-CONE-CONE-D2-D1-CONE-SES1 d-CONE-CONE-D2-D1-CONE-SES1 
		    inv-CONE-CONE-h2-h1-CONE-SES1 group-operation-CONE-CONE-H2-H1-CONE-SES1 zero-CONE-CONE-H2-H1-CONE-SES1 external-CONE-CONE-H2-H1-CONE-SES1 inverse-CONE-CONE-H2-H1-CONE-SES1 d-CONE-CONE-H2-H1-CONE-SES1    
		    Rf-CONES-CONE-SES1 Rg-CONES-CONE-SES1 RH-CONES-CONE-SES1
		    NEW-F-CONE-DI-CA  NEW-g-CONE-DI-CA NEW-H-CONE-DI-CA))

(defthm lema1
(IMPLIES
  (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
       (INV-CONE-CONE-D2-D1-CONE-SES1 N B)
       (INTEGERP N))
  (EQUAL (NEW-F-CONE-DI-CA N
                           (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B))
         (GROUP-OPERATION-CA N (NEW-F-CONE-DI-CA N A)
                             (NEW-F-CONE-DI-CA N B)))))


(defthm lema2
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INV-RING-R R)
              (INTEGERP N))
         (EQUAL (NEW-F-CONE-DI-CA N
                                  (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R A))
                (EXTERNAL-CA N R (NEW-F-CONE-DI-CA N A)))))


(defthm lema3
  (IMPLIES (INTEGERP N)
         (EQUAL (NEW-F-CONE-DI-CA N (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))
                (ZERO-CA N))))


(defthm lema4
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (EQUAL (NEW-F-CONE-DI-CA N
                                  (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N A))
                (INVERSE-CA N (NEW-F-CONE-DI-CA N A)))))


(defthm lema5
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(integerp n))
	   (INV-CA N (NEW-F-CONE-DI-CA N A))))


(defthm lema6
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(integerp n))
	   (EQUAL (D-CA N (NEW-F-CONE-DI-CA N A))
		  (NEW-F-CONE-DI-CA (+ -1 N)
				    (D-CONE-CONE-D2-D1-CONE-SES1 N A)))
	   ))


(defthm lema7
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(integerp n))
	   (INV-CONE-CONE-D2-D1-CONE-SES1 (+ 1 N)
                               (NEW-H-CONE-DI-CA N A))
	   ))


(defthm lema9
  (implies (and (INV-CA N A)
		(integerp n))
	   (INV-CONE-CONE-D2-D1-CONE-SES1 N (NEW-G-CONE-DI-CA N A))))


(defthm lema10
  (implies (and (INV-CA N A)
		(INV-CA N B)
		(INTEGERP N))
	   (EQUAL (NEW-G-CONE-DI-CA N (GROUP-OPERATION-CA N A B))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N (NEW-G-CONE-DI-CA N A)
                                                  (NEW-G-CONE-DI-CA N B)))
	   ))


(defthm lema11
  (implies (and (INV-CA N A)
		(INV-RING-R R)
		(INTEGERP N))
	   (EQUAL (NEW-G-CONE-DI-CA N (EXTERNAL-CA N R A))
       (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R (NEW-G-CONE-DI-CA N A)))))


(defthm lema12
  (implies (integerp n)
	   (EQUAL (NEW-G-CONE-DI-CA N (ZERO-CA N))
       (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))))

 


(in-theory (disable INV-CONE-CONE-D2-D1-CONE-SES1
		    ZERO-CONE-CONE-D2-D1-CONE-SES1
		    D-CONE-CONE-D2-D1-CONE-SES1
		    INVERSE-CONE-CONE-D2-D1-CONE-SES1
		    EXTERNAL-CONE-CONE-D2-D1-CONE-SES1
		    GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
		    LG-CONES-CONE-SES1
		    LF-CONES-CONE-SES1 
		    LH-CONES-CONE-SES1
		    inv-CONE-CONE-D2-D1-CONE-SES1 group-operation-CONE-CONE-D2-D1-CONE-SES1 zero-CONE-CONE-D2-D1-CONE-SES1 external-CONE-CONE-D2-D1-CONE-SES1 inverse-CONE-CONE-D2-D1-CONE-SES1 d-CONE-CONE-D2-D1-CONE-SES1 
		    inv-CONE-CONE-h2-h1-CONE-SES1 group-operation-CONE-CONE-H2-H1-CONE-SES1 zero-CONE-CONE-H2-H1-CONE-SES1 external-CONE-CONE-H2-H1-CONE-SES1 inverse-CONE-CONE-H2-H1-CONE-SES1 d-CONE-CONE-H2-H1-CONE-SES1    
		    Rf-CONES-CONE-SES1 Rg-CONES-CONE-SES1 RH-CONES-CONE-SES1
		    NEW-F-CONE-DI-CA  NEW-g-CONE-DI-CA NEW-H-CONE-DI-CA))



(defthm lema8-aux
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(integerp n))
	   (EQUAL (NEW-H-CONE-DI-CA N
                         (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N A))
		  (INVERSE-CONE-CONE-D2-D1-CONE-SES1 (+ N 1)
                                          (NEW-H-CONE-DI-CA N A)))
	   )
  :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )

(defthm lema8
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(integerp n))
	   (EQUAL (NEW-H-CONE-DI-CA N
                         (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N A))
		  (INVERSE-CONE-CONE-D2-D1-CONE-SES1 (+ 1 n)
                                          (NEW-H-CONE-DI-CA N A)))
	   )
  :hints (("Goal" :use (:instance  lema8-aux))) )

(defthm lema13-aux
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INV-CONE-CONE-D2-D1-CONE-SES1 N b)
		(integerp n))
	   (EQUAL (NEW-H-CONE-DI-CA N
                         (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 (+ N 1)
                                                  (NEW-H-CONE-DI-CA N A)
                                                  (NEW-H-CONE-DI-CA N B))))
   :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )

(defthm lema13
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INV-CONE-CONE-D2-D1-CONE-SES1 N b)
		(integerp n))
	   (EQUAL (NEW-H-CONE-DI-CA N
                         (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 N A B))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1 (+ 1 n)
                                                  (NEW-H-CONE-DI-CA N A)
                                                  (NEW-H-CONE-DI-CA N B))))
   :hints (("Goal" :use (:instance lema13-aux))) )

(defthm lema14-aux
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INV-RING-R R)
		(INTEGERP N))
	   (EQUAL (NEW-H-CONE-DI-CA N
                         (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R A))
       (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 (+ N 1)
                                           R (NEW-H-CONE-DI-CA N A))))
  :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )


(defthm lema14
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
		(INV-RING-R R)
		(INTEGERP N))
	   (EQUAL (NEW-H-CONE-DI-CA N
                         (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 N R A))
       (EXTERNAL-CONE-CONE-D2-D1-CONE-SES1 (+ 1 n)
                                           R (NEW-H-CONE-DI-CA N A))))
  :hints (("Goal" :use (:instance lema14-aux))))


(defthm lema15-aux
  (implies (integerp n)
	   (EQUAL (NEW-H-CONE-DI-CA N (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))
		  (ZERO-CONE-CONE-D2-D1-CONE-SES1 (+ N 1))))
   :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )


(defthm lema15
  (implies (integerp n)
	   (EQUAL (NEW-H-CONE-DI-CA N (ZERO-CONE-CONE-D2-D1-CONE-SES1 N))
		  (ZERO-CONE-CONE-D2-D1-CONE-SES1 (+ 1 n))))
   :hints (("Goal" :use (:instance lema15-aux))) )


(defthm lema16
  (implies (and (inv-ca n a)
		(integerp n))
	   (EQUAL (NEW-G-CONE-DI-CA N (INVERSE-CA N A))
		  (INVERSE-CONE-CONE-D2-D1-CONE-SES1 N (NEW-G-CONE-DI-CA N A))))
  :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )

   
(defthm lema17
  (implies (and (inv-ca n a)
		(integerp n))
	   (EQUAL (D-CONE-CONE-D2-D1-CONE-SES1 N (NEW-G-CONE-DI-CA N A))
		  (NEW-G-CONE-DI-CA (+ -1 N) (D-CA N A))))
   :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )


(defthm lema18
  (implies (and (INV-CONE-CONE-D2-D1-CONE-SES1 N GNRT)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
            N
            (NEW-H-CONE-DI-CA (+ -1 N)
                              (D-CONE-CONE-D2-D1-CONE-SES1 N GNRT))
            (D-CONE-CONE-D2-D1-CONE-SES1 (+ 1 N)
                                         (NEW-H-CONE-DI-CA N GNRT)))
       (GROUP-OPERATION-CONE-CONE-D2-D1-CONE-SES1
            N GNRT
            (INVERSE-CONE-CONE-D2-D1-CONE-SES1
                 N
                 (NEW-G-CONE-DI-CA N (NEW-F-CONE-DI-CA N GNRT))))))
  :hints (("Goal" :use (:instance |CMPS-REDUCTION1-REDUCTION2-is-a-reduction-CONE-DI-CA|))) )

;;;--------------------------------------------------


(in-theory (enable INV-CONE-CONE-H2-H1-CONE-SES1
		   GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1
		   D-CONE-CONE-H2-H1-CONE-SES1
		   ))



(DEFTHM GROUP-OPERATION-hB-COMMUTATIVITY
  (IMPLIES (AND (INV-HB N A)
		(INV-HB N B)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-HB N A B)
		  (GROUP-OPERATION-HB N B A))))

(DEFTHM GROUP-OPERATION-hc-COMMUTATIVITY
  (IMPLIES (AND (INV-Hc N A)
		(INV-Hc N B)
		(INTEGERP N))
	   (EQUAL (GROUP-OPERATION-Hc N A B)
		  (GROUP-OPERATION-Hc N B A))))

(defthm lema19-help
  (IMPLIES (AND (INV-hB N a)
		(INV-hB N b )
		(INV-hB N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-hB N a (GROUP-OPERATION-hB N b c))
		(GROUP-OPERATION-hB N c (GROUP-OPERATION-hB N a b))
                )) 
:hints (("Goal" :use ((:instance prop5)
		      (:instance  group-operation-hb-commutativity
				  (a c)
				  (b (GROUP-OPERATION-hB N a b)))))))


(defthm lema19-help2
  (IMPLIES (AND (INV-hc N a)
		(INV-hc N b )
		(INV-hc N c)
		(integerp n))
         (EQUAL (GROUP-OPERATION-hc N a (GROUP-OPERATION-hc N b c))
		(GROUP-OPERATION-hc N c (GROUP-OPERATION-hc N a b))
                )) 
:hints (("Goal" :use ((:instance prop7)
		      (:instance  group-operation-hc-commutativity
				  (a c)
				  (b (GROUP-OPERATION-hc N a b)))))))

(defthm lema19
  (implies (and (INV-CONE-CONE-H2-H1-CONE-SES1 N A)
		(INV-CONE-CONE-H2-H1-CONE-SES1 N b)
		(INV-CONE-CONE-H2-H1-CONE-SES1 N c)
		(integerp n))
	   (EQUAL 
       (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1
            N A
            (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1 N B C))
       (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1
            N C
            (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1 N A B))))
  )


(defthm lema20
  (implies (and (INV-CONE-CONE-H2-H1-CONE-SES1 N A)
		(integerp n))
	   (INV-CONE-CONE-H2-H1-CONE-SES1 (+ -1 N)
                               (D-CONE-CONE-H2-H1-CONE-SES1 N A))))


(defthm lema19-bis
  (IMPLIES (AND (INV-CONE-CONE-H2-H1-CONE-SES1 N A)
              (INV-CONE-CONE-H2-H1-CONE-SES1 N B)
              (INV-CONE-CONE-H2-H1-CONE-SES1 N C)
              (INTEGERP N))
         (EQUAL (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1
                     N B
                     (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1 N A C))
                (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1
                     N A
                     (GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1 N B C))))
)


(in-theory (disable INV-CONE-CONE-H2-H1-CONE-SES1
		   GROUP-OPERATION-CONE-CONE-H2-H1-CONE-SES1
		   D-CONE-CONE-H2-H1-CONE-SES1))


(defthm lema21-aux
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1 (+ N 1)
                                        (RH-CONES-CONE-SES1 N A)))
  :hints (("Goal" :use (:instance |HOMOTOPY-EQUIVALENCE-CONES-is-an-homotopy-equivalence-CONE-SES1|))))

(defthm lema21
  (IMPLIES (AND (INV-CONE-CONE-D2-D1-CONE-SES1 N A)
              (INTEGERP N))
         (INV-CONE-CONE-D2-D1-CONE-SES1 (+ 1 n)
                                        (RH-CONES-CONE-SES1 N A)))
  :hints (("Goal" :use (:instance lema21-aux))))





(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
   'inv-CONE-CONE-D2-D1-CONE-SES1 'group-operation-CONE-CONE-D2-D1-CONE-SES1 'zero-CONE-CONE-D2-D1-CONE-SES1 'external-CONE-CONE-D2-D1-CONE-SES1 'inverse-CONE-CONE-D2-D1-CONE-SES1 'd-CONE-CONE-D2-D1-CONE-SES1 
   ) 
  (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
   'inv-CA 'group-operation-CA 'zero-CA 'external-CA 'inverse-CA 'd-CA)
  'NEW-F-CONE-DI-CA  'NEW-g-CONE-DI-CA 'NEW-H-CONE-DI-CA
  )
 (reduction 
 (chain-complex 
  'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R 
    'inv-CONE-CONE-D2-D1-CONE-SES1 'group-operation-CONE-CONE-D2-D1-CONE-SES1 'zero-CONE-CONE-D2-D1-CONE-SES1 'external-CONE-CONE-D2-D1-CONE-SES1 'inverse-CONE-CONE-D2-D1-CONE-SES1 'd-CONE-CONE-D2-D1-CONE-SES1 
   )
 (chain-complex 
   'inv-ring-R 'addition-ring-R 'zero-element-R 'inverse-R 'product-ring-R 'unit-R
   'inv-CONE-CONE-h2-h1-CONE-SES1 'group-operation-CONE-CONE-H2-H1-CONE-SES1 'zero-CONE-CONE-H2-H1-CONE-SES1 'external-CONE-CONE-H2-H1-CONE-SES1 'inverse-CONE-CONE-H2-H1-CONE-SES1 'd-CONE-CONE-H2-H1-CONE-SES1)
  'Rf-CONES-CONE-SES1 'Rg-CONES-CONE-SES1 'RH-CONES-CONE-SES1
  ))
 'homotopy-equivalence-A
   )













